\begin{tabbing}
d{-}machine($i$;$M$;${\it dec}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$<$${\it dec}$\+
\\[0ex], $\lambda$$k$,$v$,$s$,$x$. if islocal($k$) $\vee_{b}$destination(lnk($k$)) = $i$
\\[0ex]then $M$.ef($k$,$x$,read{-}state($s$),$v$)?$s$($x$)
\\[0ex]else $s$($x$)
\\[0ex]fi 
\\[0ex], $\lambda$$k$,$v$,$s$. if islocal($k$) $\vee_{b}$destination(lnk($k$)) = $i$
\\[0ex]then filter($\lambda$$m$.source(mlnk($m$)) = $i$;$M$.sends($k$,$s$,$v$))
\\[0ex]else []
\\[0ex]fi $>$
\-
\end{tabbing}